It seems that pushing/popping operations are exposed via IsSymBackend. Ideally, we would only expose operations that automatically enforce the desired matching push/pop condition (basically, just an operation like inFreshFrame). However, I'm not really familiar with the code that uses this API (Lang.Crucible.Backend.Online), and it's not clear to me how feasible it would be to refactor it to fit this pattern. However, I think the current PR is already an improvement, in that it makes it possible to avoid panicing functions in the public API.